/* -*- Mode: C++; c-basic-offset: 2 -*- */

#ifndef __TERN_BC_LIB
#define __TERN_BC_LIB

#include "llvm/Function.h"

#include "klee/ExecutionState.h"
#include "Executor.h"

/// \todo Should move to SpecialFunctionHandler.cpp

namespace klee {
  class BcLib {

  public:
    bool callDLFunction(ExecutionState &state,
                        KInstruction *target,
                        llvm::Function *function,
                        std::vector< ref<Expr> > &arguments);

    BcLib (Executor &_executor);

  private:
    void callDLOpen(ExecutionState &state,
                    KInstruction *target,
                    llvm::Function *function,
                    std::vector< ref<Expr> > &arguments);
    void callDLSym(ExecutionState &state,
                   KInstruction *target,
                   llvm::Function *function,
                   std::vector< ref<Expr> > &arguments);
    void callDLClose(ExecutionState &state,
                     KInstruction *target,
                     llvm::Function *function,
                     std::vector< ref<Expr> > &arguments);
    bool isBcFile(ExecutionState &state, 
                  ref<Expr> path);
    bool isBcHandle(ExecutionState &state,
                    ref<Expr> handle);

    class Executor &executor;
  };


}

#endif
